Nuprl Lemma : normal-es-dt
0,22
postcript
pdf
da
:
k
:Knd fp
Type,
l
:IdLnk. Normal(
da
)
Normal(dt(
l
;
da
))
latex
Definitions
t
T
,
x
:
A
.
B
(
x
)
,
rcv(
l
,
tg
)
,
P
&
Q
,
P
Q
,
b
,
x
dom(
f
).
v
=
f
(
x
)
P
(
x
;
v
)
,
Normal(
T
)
,
Normal(
da
)
,
x
:
A
B
(
x
)
,
Knd
,
Type
,
f
(
x
)
,
AtomFree(
T
;
x
)
,
Void
,
x
:
A
.
B
(
x
)
,
Top
,
x
:
A
B
(
x
)
,
P
Q
,
Id
,
dt(
l
;
da
)
,
x
.
A
(
x
)
,
x
.
t
(
x
)
,
a
:
A
fp
B
(
a
)
,
IdDeq
,
x
dom(
f
)
,
Normal(
ds
)
,
IdLnk
Lemmas
normal-da
wf
,
IdLnk
wf
,
fpf
wf
,
Knd
wf
,
assert
wf
,
fpf-dom
wf
,
id-deq
wf
,
fpf-trivial-subtype-top
,
es-dt
wf
,
Id
wf
,
es-dt-dom
,
es-dt-ap
,
rcv
wf
origin
da:k:Knd fp
Type, l:IdLnk. Normal(da) 
Normal(dt(l;da)) da:k:Knd fp Type, l:IdLnk. Normal(da) Normal(dt(l;da)) 
Tx:A. B(x) Q
bxdom(f). v=f(x) P(x;v)
B(x)
x:A. B(x)
B(x)
Q
x.A(x)
x. t(x) B(a) dom(f)